﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace PSZT
{
    public class Formula
    {
        public List<Predykat> przeslanki = new List<Predykat>();
        public Predykat konkluzja;
        //public bool czyAtom = false; //jezeli wartosc jest prawdą to
                      //lista przeslanek jest pusta a danym literalem jest konkluzja
        public int ogolnosc
        {
            get
            {
                List<string> uzyteZmienne = new List<string>();
                foreach (Predykat p in przeslanki)
                {
                    foreach (string arg in p.argumenty)
                    {
                        if (Predykat.czyZmienna(arg) && !uzyteZmienne.Contains(arg))
                        {
                            uzyteZmienne.Add(arg);
                        }
                    }
                }
                return uzyteZmienne.Count;
            }
        }

        override public string ToString()
        {
            string ret = "";
            if (przeslanki.Count > 0)
            {
                foreach (Predykat pred in przeslanki)
                {
                    ret += pred.ToString() + " ^ ";
                }
                ret = ret.Remove(ret.Count() - 2);
                ret += "=> " + konkluzja.ToString();
                return ret;
            }
            else
            {
                ret = konkluzja.ToString();
                return ret;
            }
        }

        public bool czyLiteral()
        {
            return przeslanki.Count == 0;
        }

        public override bool Equals(object obj)
        {
            if (this.GetType() != obj.GetType())
                return false;

            Formula f = obj as Formula;
            if (f.konkluzja.Equals(this.konkluzja) && f.przeslanki.SequenceEqual(this.przeslanki))
            {
                return true;
            }

            return false;
        }
    }

}
